# -*- Mode: makefile -*-
# Makefile.in for building and using the CCured compiler 
# @do_not_edit@ Makefile.in
#  
# toplevel Makefile for CCured project
# authors: George Necula, Scott McPeak
# 
include cil/config.mk

# tweak to provoke commit..

# Just a target to be used by default
.PHONY: setup quickbuild all doc distrib ccured libraries
setup: 
	$(MAKE) -C cil 
	$(MAKE) ccured libraries  _GNUCC=1 NATIVECAML= 
ifdef BUILD_RELEASEPG
	$(MAKE) ccured libraries  _GNUCC=1 NATIVECAML=1 RELEASELIB=1 USE_PG=1
endif
	$(MAKE) ccured libraries  _GNUCC=1 NATIVECAML=1 RELEASELIB=1
ifeq ($(HAS_MSVC), yes)
	$(MAKE) libraries _MSVC=1 NATIVECAML=
	$(MAKE) libraries _MSVC=1 NATIVECAML=1 RELEASELIB=1
endif



# sfg: I think I need "make all" to do "make cil_setup" for automake purposes
all: cil_setup


quickbuild: cil_setup ccuredversion ccured libraries

cil_setup:
	$(MAKE) -C cil setup

# look out for outdated Makefile; if it's out of date, this will automatically
# re-run ./config.status, then re-exec make with the same arguments
Makefile: config.status Makefile.in
	./$<

config.status: configure
	./$@ --recheck

configure: configure.in
	autoconf

####
#### OCAML stuff
####
# Debugging. Set ECHO= to debug this Makefile 
ECHO := @

ifdef RELEASE
  NATIVECAML := 1
  UNSAFE     := 1
endif


# Put here all the byproducts of make
OBJDIR      := obj/$(ARCHOS)
DEPENDDIR   := obj/.depend

# First stuff that makes the executable 

CCURED_MODULES  := ccuredversion ptrnode globinit cxxpp \
                   markutil \
                   poly wrappers dependent depfunc taggedunion vararg \
                   curesplit curestats stackoverflow \
                   optutil curechecks cure markcxx markptr cfg \
                   solveutil unionfind type typecheck solver optim seoptim \
                   choptim \
                   elimabc intset \
                   dominator annot astslicer simplemem \
                   heap partial verify main

MODULES        = $(CCURED_MODULES)
SOURCEDIRS     := src cil/src/ext cil/ocamlutil
MLLS           := 
MLYS           := 

COMPILEFLAGS = -I cil/obj/$(ARCHOS)
LINKFLAGS    = -I cil/obj/$(ARCHOS)

# Include now the common set of rules for OCAML
include cil/ocamlutil/Makefile.ocaml

   # Now the rule to make ccured

PROJECT_EXECUTABLE = $(OBJDIR)/ccured$(EXE)
PROJECT_MODULES    = $(CCURED_MODULES)
PROJECT_CMODULES   = 
PROJECT_LIBS       = unix str cil
.PHONY: ccured
ifneq ($(ARCHOS), ppc_DARWIN)
ccured: $(PROJECT_EXECUTABLE)
else
ccured:
	@echo "CCured does not currently bulid on powerpc-darwin systems."
endif
#include ocamlutil/Makefile.ocaml.build
$(PROJECT_EXECUTABLE) : $(PROJECT_MODULES:%=$(OBJDIR)/%.$(CMO)) \
                        $(PROJECT_CMODULES:%=$(OBJDIR)/%.$(CMC))
	@$(NARRATIVE) "Linking $(COMPILETOWHAT) $@ $(LINKMSG)"
	$(AT)$(CAMLLINK) -verbose -o $@ \
                    $(PROJECT_LIBS:%=%.$(CMXA)) \
                    $^


ifndef CCUREDHOME
  CCUREDHOME=@CCUREDHOME@
endif

# Now do the user-specific customization
# It is Ok if this file does not exist
# GN. Let's try to get rid of this.
# sm: but I like/need it!
-include $(CCUREDHOME)/.ccuredrc

# Set the compiler
ifndef _MSVC
  ifndef _GNUCC 
     @DEFAULT_COMPILER@=1
  endif
endif

# Now include the compiler specific stuff
ifdef _MSVC
  include Makefile.msvc
else
  ifdef _GNUCC
    include Makefile.gcc
  endif
endif

# sm: separating release library from release tools
ifdef RELEASELIB
  COMPILEREXT := $(COMPILERNAME)_releaselib
else
  COMPILEREXT := $(COMPILERNAME)_debug
endif

# dsw: allow use of -pg flag
ifdef USE_PG
  COMPILEREXT := $(COMPILEREXT)pg
endif

GCDIR := $(CCUREDHOME)/lib/gc/$(COMPILERNAME)
GCLIB := $(GCDIR)/gc.$(LIBEXT)
GCMAKE := $(MAKE) -C $(GCDIR) 
ifdef _MSVC 
  GCMAKE += -f Makefile.msvc srcdir=..
endif
# pretend it's only dependent on one file; that's not true of course,
# but we rarely (ever?) modify the gc's sources, and one dependency
# is better than none (which causes recompile every time!)
$(GCLIB): $(CCUREDHOME)/lib/gc/mark.c
	$(GCMAKE)
	cd $(CCUREDHOME)/lib/gc/$(COMPILERNAME); \
            rm -f gc.log; ./gctest; if test -f gc.log ;then cat gc.log; fi


testgc:
	rm -f $(GCLIB)
	$(MAKE)
	objdump --syms $(CCUREDLIB) | grep GC_



#
# Create the version information module
.PHONY: ccuredversion 
ccuredversion: $(OBJDIR)/ccuredversion.ml
$(OBJDIR)/ccuredversion.ml: configure.in Makefile.in
	rm -f $@
	echo "(* This module was generated automatically by code in Makefile *)" >$@
# Generate here the version information
	echo "let ccuredVersionMajor = @CCURED_VERSION_MAJOR@" >>$@
	echo "let ccuredVersionMinor = @CCURED_VERSION_MINOR@" >>$@
	echo "let ccuredVersionRev   = @CCURED_VERSION_REV@"   >>$@
	echo "let ccuredVersion      = \"@CCURED_VERSION@\""  >>$@ 

###
###
###    # Now the rules to make the library
###
###
CCUREDLIB := $(OBJDIR)/ccured_$(COMPILEREXT).$(LIBEXT)

CCUREDLIBARG :=

# RELEASELIB means we try for performance, with terse error messages
# !RELEASELIB means enable more debugging checking, and try to produce
#             better error messages
ifdef RELEASELIB
  CCUREDLIBARG += $(DEF)RELEASELIB
endif

# dsw: use -pg for profiling
ifdef USE_PG
  CCUREDLIBARG += -pg
endif

# _DEBUG means to try to drop into the debugger on failure
ifndef RELEASELIB
  CCUREDLIBARG += $(DEF)_DEBUG
endif

# NO_FPFAIL_SYSLOG means the syslog(2) call in ccuredlib.c will be omitted
ifdef NO_FPFAIL_SYSLOG
  CCUREDLIBARG += $(DEF)NO_FPFAIL_SYSLOG
endif

ifdef NO_TAGS
  CCUREDLIBARG += $(DEF)NO_TAGS
endif

# when this is set, it disables the check for writing a stack pointer,
# and also disables the effect of the __HEAPIFY annotation; it makes
# the resulting Curing unsound, but is useful for measuring performance
# or for temporarily getting past a "Stack pointer" failure
# GN: There are other ways to get past a Stack pointer failure !!
ifdef DISABLE_HEAPIFY
  CCUREDLIBARG += $(DEF)DISABLE_HEAPIFY
endif

# we build the library from source each time, so that we don't end up
# with .o files built with Makefile arguments that have changed
$(CCUREDLIB): lib/ccuredlib.c include/ccured.h include/ccuredannot.h \
                              include/ccuredcheck.h $(GCLIB) 
	@echo "Trying to build $(CCUREDLIB)"
	@true "CCUREDLIBARG is $(CCUREDLIBARG)"
	@true "CFLAGS is $(CFLAGS)"
	$(CC) $(CFLAGS) $(INC)./include $(CONLY) $(CCUREDLIBARG) \
                    $(OBJOUT)$(OBJDIR)/ccuredlib.$(OBJEXT) lib/ccuredlib.c
ifdef _GNUCC
	cp -f $(GCLIB) $@
	ar -rs $@            $(OBJDIR)/ccuredlib.$(OBJEXT) 
else
	$(AR) $(LIBOUT)$@ $(GCLIB) $(OBJDIR)/ccuredlib.$(OBJEXT) 
endif

# we need to know what the patcher will think the compiler's version is

PATCHER := LANG=C perl $(CCUREDHOME)/cil/bin/patcher --mode=$(COMPILERNAME)
COMPILERVERSION := $(shell $(PATCHER) --dumpversion)

# names all of the patched include files, so we can have a proper dependency
# The PATCH_SYSINCLUDES is in Makefile.gcc
PATCHEDHEADERSDIR := $(CCUREDHOME)/include/$(COMPILERVERSION)
PATCHEDHEADERS := $(foreach file, $(PATCH_SYSINCLUDES), $(PATCHEDHEADERSDIR)/$(file))


# the patch template file
PATCHTEMPLATE := $(CCUREDHOME)/include/ccured_$(COMPILERNAME).patch

.PHONY: patched-headers
patched-headers: $(PATCHEDHEADERS)
$(PATCHEDHEADERS): $(PATCHEDHEADERSDIR)/stamp
$(PATCHEDHEADERSDIR)/stamp: $(CCUREDHOME)/cil/bin/patcher $(PATCHTEMPLATE)
#       throw away all the existing patched includes
	$(PATCHER) --dest=$(CCUREDHOME)/include --clean
#       now re-regenerate them
	$(PATCHER) --patch=$(PATCHTEMPLATE) \
                   --dest=$(CCUREDHOME)/include \
	           $(foreach file,$(PATCH_SYSINCLUDES), --sfile=$(file))
	touch $@

ifneq ($(ARCHOS), ppc_DARWIN)
libraries: $(CCUREDLIB) patched-headers
else
libraries:
	@echo "CCured libraries do not currently bulid on powerpc-darwin systems."
endif


###
### DOCUMENTATION
###
doc: ccured-doc

ifeq ($(ARCHOS), x86_WIN32)
 HEVEA:=hevea
 # The image generation does not work on cygwin!
 IMAGEN:=true
else
 HEVEA:= hevea -exec xxdate.exe
 IMAGEN:=imagen
endif

# if you do not want the code example processed defien an environemnt
# varable NO_EXAMPLES=1
ccured-doc:
ifdef NO_EXAMPLES
# Delete everything
	-rm -rf doc/html/ccured
else
# Delete everything except examples
	-rm -f doc/html/ccured
endif
# Try to make the directories, if they do not exist
	-mkdir doc/html/ccured
	-mkdir doc/html/ccured/examples
# Create the version document
# 	cd doc/html/ccured; echo "\def\cilversion{@CIL_VERSION@}" >ccured.version.tex
	cd doc/html/ccured; echo "\def\ccuredversion{@CCURED_VERSION@}" >>ccured.version.tex
	cd doc; perl ccuredcode.pl ccured.tex ccuredpp.tex
	cd doc/html/ccured; $(HEVEA) ../../ccuredpp; $(HEVEA) ../../ccuredpp
	if test -f doc/html/ccured/ccuredpp.image.tex ;then \
         cp doc/hevea.sty doc/comment.sty doc/*.eps doc/html/ccured; \
         cd doc/html/ccured; $(IMAGEN) ccuredpp \
        ;fi
	cp include/ccured.h doc/html/ccured
	cp include/ccuredcheck.h doc/html/ccured
	cd doc/html/ccured; mv ccuredpp.html ccured.html
	cd doc/html/ccured; hacha -o ccuredtoc.html ccured.html
	cd doc/html/ccured; $(HEVEA) ../../setup; $(HEVEA) ../../setup
	cd doc/html/ccured; $(HEVEA) ../../cvssetup; $(HEVEA) ../../cvssetup
	cp doc/index.html doc/html/ccured/index.html
	cp doc/ccuredheader.html doc/html/ccured
	cp lib/browser_help.html doc/html/ccured
	cp lib/bullet.gif doc/html/ccured

###
### Cleaning
###
# sm: removed the *_all*.c case because it was deleting my
# combine_node_alloc_[12].c files.. if I can find out what that was
# supposed to delete, I'll add back in a more specific wildcard
clean: cleancaml
	$(PATCHER) --dest=$(CCUREDHOME)/include --clean
	rm -f $(OBJDIR)/ccured_*
	$(MAKE) -C $(CCUREDHOME)/lib/gc clean
	cd $(CCUREDHOME)/lib/gc; \
	     	rm -f $(foreach COMP, GNUCC MSVC, \
                     $(foreach EXT, exe o a obj lib, $(COMP)/*.$(EXT)))
	-find test \( \
		-name '*cil.c' -o \
		-name '*cured.c' -o \
                -name '*cured.*optim.c' -o \
		-name '*.exe' -o \
		-name '*.i' -o \
		-name '*_ppp.c' -o \
		-name '*.origi' -o \
		-name '*.o' -o \
		-name '*.obj' -o \
		-name '*cabs.c' -o \
		-name '*infer.c' -o \
		-name '*_comb*.c' \
	\) -exec rm {} \;
	rm -f src/frontc/clexer.ml
	rm -f src/formatlex.ml
	rm -f src/frontc/cparser.{ml,mli,output}
	rm -f src/formatparse.{ml,mli,output}

# sm: these last four commands remove the byproducts of running ocamllex
# and ocamlyacc; ordinarily they get moved into .obj, but if I cancel a
# build partway then sometimes empty files get left behind (and this
# breaks the build)


##################
###
### CREATE THE DISTRIBUTION
###
#################
DISTRIB_DIR:= TEMP_ccured-distrib

.PHONY: distrib distrib-nocheck checkdistrib
CCURED_TAR_GZ:=ccured-@CCURED_VERSION@.tar.gz

# The next file is created in test/Makefile (make sure we use the same name)
CCUREDTESTS_TAR_GZ:=ccured-tests-@CCURED_VERSION@.tar.gz

distrib: distrib-nocheck checkdistrib
	@echo

# A CCured distribution includes a CIL distribution
# Reuse configure and Makefile.ocaml stuff from CIL distribution
# We need to specify here only the files that are not distributed with CIL
D_ROOT := configure configure.in config.h.in \
	  install-sh config.guess config.sub \
	  Makefile.in LICENSE \
          Makefile.gcc Makefile.msvc

D_CIL_EXT := oneret.ml oneret.mli optutil.ml optutil.mli

D_LIB := Makefile CCured.pm ccuredlib.c \
        gc \
	browser_code.js browser_blank.html browser_form.html \
        browser_index.html bullet.gif pixel.gif browser_help.html \
        styles.css

D_BIN := ccured ccured.bat.in

QUICKTESTS   := array1 array2 alloc bitfield cast1 globals
QUICKTESTS_R := hello funptr1 vararg1

D_TEST   := Makefile
D_TEST_SMALL1 := testharness.h $(patsubst %,%.c,$(QUICKTESTS) $(QUICKTESTS_R))

CIL_VERSION=@CCURED_VERSION@

distrib-nocheck: doc
	rm -f $(CCURED_TAR_GZ)
# Make (without checking so that we do not have garbage) a CIL distribution
	$(MAKE) -C cil distrib-nocheck
# Unpack the CIL distribution in our temporary directory
	rm -rf $(DISTRIB_DIR)
	mkdir -p $(DISTRIB_DIR)/ccured
	cd $(DISTRIB_DIR)/ccured; tar xvfz ../../cil/cil-$(CIL_VERSION).tar.gz
# Delete all the documentation
	rm -rf $(DISTRIB_DIR)/ccured/doc/*
# And copy it again from our own copy
	cp -r doc/html/ccured $(DISTRIB_DIR)/ccured/doc
# Now add the CCured-specific stuff
	cd $(DISTRIB_DIR)/ccured; mkdir include src lib bin test test/small1
	cp include/*.h $(DISTRIB_DIR)/ccured/include 
	cp include/*.patch $(DISTRIB_DIR)/ccured/include 
	mkdir $(DISTRIB_DIR)/ccured/include/functions
	cp include/functions/*.h $(DISTRIB_DIR)/ccured/include/functions
	cp $(D_ROOT) $(DISTRIB_DIR)/ccured
	cp src/[a-z]*.ml src/[a-z]*.mli $(DISTRIB_DIR)/ccured/src
	cp $(patsubst %,cil/src/ext/%,$(D_CIL_EXT)) $(DISTRIB_DIR)/ccured/src
# Copy the GC sources
	$(MAKE) -C lib/gc clean
	cd lib/gc; \
	     	rm -f $(foreach COMP, GNUCC MSVC, \
                     $(foreach EXT, exe o a obj lib, $(COMP)/*.$(EXT)))
	cp -r $(patsubst %,lib/%,$(D_LIB)) $(DISTRIB_DIR)/ccured/lib
	cp -r $(patsubst %,bin/%,$(D_BIN)) $(DISTRIB_DIR)/ccured/bin
# Now the tests
	cat test/Makefile \
	    | sed -e 's|TESTDIR := ../ciltests|TESTDIR := .|g' \
            > $(DISTRIB_DIR)/ccured/test/Makefile
	cp $(patsubst %,ciltests/small1/%,$(D_TEST_SMALL1)) \
	  $(DISTRIB_DIR)/ccured/test/small1
# Delete all CVS directories
	if find $(DISTRIB_DIR) -name CVS -print >cvss.txt ; then \
            echo `cat cvss.txt` ;fi
	rm -f cvss.txt
# Now make the TAR ball
	cd $(DISTRIB_DIR); tar cfz $(CCURED_TAR_GZ) ccured
	mv $(DISTRIB_DIR)/$(CCURED_TAR_GZ) .


## Check a distribution
checkdistrib:
	cd $(DISTRIB_DIR)/ccured && ./configure && $(MAKE) && $(MAKE) quicktest

checktestdistrib:
	cd $(DISTRIB_DIR)/ccured/test && testsafec --run --group inferbox --nogroup slow

## Publish the distribution
CCUREDHTMLDEST := /var/www/ccured
publish_distrib: publish_doc
	if test -d $(CCUREDHTMLDEST); then \
           cp -f $(CCURED_TAR_GZ) $(CCUREDHTMLDEST)/distrib; \
           ln -sf $(CCUREDHTMLDEST)/distrib/$(CCURED_TAR_GZ) $(CCUREDHTMLDEST)/distrib/ccured-latest.tar.gz ; \
	else \
	   error "Cannot publish because $(CCUREDHTMLDEST) does not exist" ; \
        fi
           # cp -f $(CCUREDTESTS_TAR_GZ) $(CCUREDHTMLDEST)/distrib; \
           # ln -sf $(CCUREDHTMLDEST)/distrib/$(CCUREDTESTS_TAR_GZ) $(CCUREDHTMLDEST)/distrib/ccured-tests-latest.tar.gz ; \


.PHONY: publish_doc
publish_doc: doc
	if test -d $(CCUREDHTMLDEST); then \
           cp -rf doc/html/ccured/* $(CCUREDHTMLDEST); \
	else \
	   error "Cannot publish because $(CCUREDHTMLDIST) does not exist" ; \
        fi

##
## The test cases have been moved to test/Makefile
##

### We still have a quick test
quicktest: 
	$(MAKE) -C test INFERBOX=infer $(patsubst %, test/%, $(QUICKTESTS))
	$(MAKE) -C test INFERBOX=infer $(patsubst %, testrun/%, $(QUICKTESTS_R))

check: quicktest

# sm: make a file that lists all our sources, for easy grepping
ALLSRCEXTS=-name '*.c' -o -name '*.h' -o -name '*.pl' -o -name '*.ml' \
           -o -name '*.mli' -o -name '*.pm'
.PHONY: allsrcs
allsrcs:
	find src $(ALLSRCEXTS) > allsrcs
	find bin $(ALLSRCEXTS) >> allsrcs
	find include -name '*_wrappers.h' >> allsrcs
	find lib $(ALLSRCEXTS) | grep -v '^lib/gc/' >> allsrcs 
	ls test/Makefile.in Makefile.in include/*.patch >> allsrcs


# Install the web interface
installweb: setup $(CCUREDHTMLDEST)
# Copy over the files needed for running CCured
	mkdir -p $(CCUREDHTMLDEST)/bin
	cp $(foreach f, ccured, \
                     bin/$(f)) \
           $(CCUREDHTMLDEST)/bin
# Now copy over CilConfig.pm but change the directory names
	cat bin/CilConfig.pm | sed -e 's|@CILHOME@|$(CCUREDHTMLDEST)|g' \
              >$(CCUREDHTMLDEST)/bin/CilConfig.pm
	mkdir -p $(CCUREDHTMLDEST)/obj/@ARCHOS@
	cp $(foreach f, ccured.asm.exe ccured_GNUCC_releaselib.a, \
                     obj/@ARCHOS@/$(f)) \
           $(CCUREDHTMLDEST)/obj/@ARCHOS@
	mkdir -p $(CCUREDHTMLDEST)/lib
	cp $(foreach f, $(DISTRIB_LIB) \
                        Cilly.pm CCured.pm KeptFile.pm \
                        TempFile.pm OutputFile.pm \
                        browser_blank.html browser_code.js \
                        browser_help.html browser_index.html bullet.gif \
                        browser_form.html pixel.gif styles.css, \
                     lib/$(f)) \
          $(CCUREDHTMLDEST)/lib
	mkdir -p $(CCUREDHTMLDEST)/include
	cp -r include $(CCUREDHTMLDEST)
	mkdir -p $(CCUREDHTMLDEST)/web/tmp
	chmod a+wx $(CCUREDHTMLDEST)/web/tmp
	cp $(foreach f, .htaccess web-driver.cgi index.html, \
                     web/$(f)) \
           $(CCUREDHTMLDEST)/web
	mkdir -p $(CCUREDHTMLDEST)/test/small1
	chmod a+w $(CCUREDHTMLDEST)/test/small1
	cp $(foreach f, testharness.h testkinds.h hello.c fseq1.c \
                        array2.c failnull1.c failprintf1.c failprintf2.c \
                        failprintf4.c failubound1.c func4.c list.c \
                        polyapply1.c wild2.c , \
                     test/small1/$(f)) \
           $(CCUREDHTMLDEST)/test/small1

### END


